w:World. FairFifo  (e:E, x:Id. state_after(e).x = (x after e)  vartype(loc(e);x)) 

latex

Definitions	t  T, x:A. B(x), P  Q, s.x, World, FairFifo, E, Id, state_after(e), <a, b>, , x:AB(x), s = t, loc(e), vartype(i;x)
Lemmas	Id wf, w-E wf, fair-fifo wf, world wf, w-after-lemma, subtype rel self, w-vartype wf, w-loc wf